Nuprl Lemma : d-realizes_wf
11,40
postcript
pdf
D
:dsys{i:l},
P
:({
es
:ES{i}| d-es{i:l}(
D
;
es
)}
{i'}). d-realizes{i:l}(
D
;
es
.
P
(
es
))
{i''}
latex
Definitions
x
:
A
.
B
(
x
)
,
,
t
T
,
D
realizes
es
.
P
(
es
)
,
x
(
s
)
,
P
Q
,
es
is an event system of
D
,
x
:
A
.
B
(
x
)
,
P
&
Q
Lemmas
dsys
wf
,
d-sub
wf
,
world
wf
,
fair-fifo
wf
,
possible-world
wf
,
event
system
wf
,
d-es
wf
,
w-es
wf
,
possible-world-monotonic
origin
D:dsys{i:l}, P:({es:ES{i}| d-es{i:l}(D; es)} 
{i'}). d-realizes{i:l}(D; es.P(es)) 
{i''} D:dsys{i:l}, P:({es:ES{i}| d-es{i:l}(D; es)} {i'}). d-realizes{i:l}(D; es.P(es)) {i''} x:A. B(x) T
Q
x:A. B(x)